Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

The replacement map contains the following entries:

eq: empty set
0: empty set
true: empty set
s: empty set
false: empty set
inf: {1}
cons: empty set
take: {1, 2}
nil: empty set
length: {1}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

The replacement map contains the following entries:

eq: empty set
0: empty set
true: empty set
s: empty set
false: empty set
inf: {1}
cons: empty set
take: {1, 2}
nil: empty set
length: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {inf, take, length, INF, TAKE, LENGTH} are replacing on all positions.
The symbols in {eq, s, cons, EQ, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

EQ(s(X), s(Y)) → EQ(X, Y)


The hidden terms of R are:

inf(s(X))
take(X, L)
length(L)

Every hiding context is built from:

take on positions {1, 2}
length on positions {1}

Hence, the new unhiding pairs DPu are :

U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(length(x_0)) → U(x_0)
U(inf(s(X))) → INF(s(X))
U(take(X, L)) → TAKE(X, L)
U(length(L)) → LENGTH(L)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 3 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {inf, take, length} are replacing on all positions.
The symbols in {eq, s, cons, U} are not replacing on any position.

The TRS P consists of the following rules:

U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(length(x_0)) → U(x_0)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(length(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ PIsEmptyProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {inf, take, length} are replacing on all positions.
The symbols in {eq, s, cons} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {inf, take, length} are replacing on all positions.
The symbols in {eq, s, cons, EQ} are not replacing on any position.

The TRS P consists of the following rules:

EQ(s(X), s(Y)) → EQ(X, Y)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(s(X), s(Y)) → eq(X, Y)
eq(X, Y) → false
inf(X) → cons(X, inf(s(X)))
take(0, X) → nil
take(s(X), cons(Y, L)) → cons(Y, take(X, L))
length(nil) → 0
length(cons(X, L)) → s(length(L))

Q is empty.

The following rules are not useable and can be deleted:

eq(0, 0) → true
eq(s(x0), s(x1)) → eq(x0, x1)
eq(x0, x1) → false
inf(x0) → cons(x0, inf(s(x0)))
take(0, x0) → nil
take(s(x0), cons(x1, x2)) → cons(x1, take(x0, x2))
length(nil) → 0
length(cons(x0, x1)) → s(length(x1))


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, EQ} are not replacing on any position.

The TRS P consists of the following rules:

EQ(s(X), s(Y)) → EQ(X, Y)

R is empty.
Q is empty.

Using the order
Polynomial interpretation [25]:

POL(EQ(x1, x2)) = x2   
POL(s(x1)) = 2 + 2·x1   

the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

EQ(s(X), s(Y)) → EQ(X, Y)

could be oriented strictly and thus removed.
All pairs have been removed.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

R is empty.
Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.